(set-logic QF_UF)
(declare-sort utt$8 0)
(declare-fun y$2 () Bool)
(declare-fun y$Counter$next () utt$8)
(declare-fun y$Counter$next_rhs_op () utt$8)
(declare-fun y$n0s8 () utt$8)
(declare-fun y$n1s8 () utt$8)
(declare-fun y$n255s8 () utt$8)
(declare-fun y$n63s8 () utt$8)
(declare-fun y$n7s8 () utt$8)
(declare-fun y$s$24_op () utt$8)
(declare-fun y$s$28_op () utt$8)
(declare-fun y$s$29_op () utt$8)
(declare-fun y$s$4_op () utt$8)
(declare-fun y$s$5_op () utt$8)
(declare-fun y$s$6_op () utt$8)
(assert (= y$s$28_op (ite y$2 y$n63s8 y$s$24_op)))
(assert (= y$s$29_op (ite y$2 y$n7s8 y$s$24_op)))
(assert (= y$s$4_op (ite false y$s$28_op y$s$29_op)))
(assert (= y$s$6_op (ite true y$s$4_op y$s$5_op)))
(assert (= y$Counter$next_rhs_op (ite false y$n0s8 y$s$6_op)))
(assert (= true (= y$Counter$next y$Counter$next_rhs_op)))
(assert (= false (not (= y$n255s8 y$Counter$next))))
(assert (distinct y$n0s8 y$n63s8 y$n1s8 y$n7s8 y$n255s8))
(check-sat)
(exit)
